(set-logic BV)
(synth-fun f ( (x (BitVec 64)) ) (BitVec 64)
((Start (BitVec 64)
((bvnot Start)
(bvxor Start Start)
(bvand Start Start)
(bvor Start Start)
(bvneg Start)
(bvadd Start Start)
(bvmul Start Start)
(bvudiv Start Start)
(bvurem Start Start)
(bvlshr Start Start)
(bvashr Start Start)
(bvshl Start Start)
(bvsdiv Start Start)
(bvsrem Start Start)
(bvsub Start Start)
x
#x0000000000000000
#x0000000000000001
#x0000000000000002
#x0000000000000003
#x0000000000000004
#x0000000000000005
#x0000000000000006
#x0000000000000007
#x0000000000000008
#x0000000000000009
#x0000000000000009
#x0000000000000009
#x000000000000000A
#x000000000000000B
#x000000000000000C
#x000000000000000D
#x000000000000000E
#x000000000000000F
#x0000000000000010
(ite StartBool Start Start)
))
(StartBool Bool
((= Start Start)
(not StartBool)
(and StartBool StartBool)
(or StartBool StartBool)
))))
(constraint (= (f #xb04b878080d1ca5c) #x0000000000000002))
(constraint (= (f #xa8c7ee4d3e00306d) #xfffffffffffffffd))
(constraint (= (f #x0185c6c8c08a7906) #x0000000000000002))
(constraint (= (f #xaca6e9b4ec36e0ae) #x0000000000000002))
(constraint (= (f #x271ec64216bd1bbb) #xfffffffffffffffd))
(constraint (= (f #x542c0898382e5e3d) #xfffffffffffffffd))
(constraint (= (f #xc85a4aed1506b688) #x0000000000000002))
(constraint (= (f #xc05b46c2ee7edecc) #x0000000000000002))
(constraint (= (f #xe3d24667b717a9cb) #xfffffffffffffffd))
(constraint (= (f #xd6e9666e12ce2e7e) #x0000000000000002))
(constraint (= (f #x986819b5e30585eb) #xfffffffffffffffd))
(constraint (= (f #x4e03d818b08a4c91) #xfffffffffffffffd))
(constraint (= (f #x7e2694738a8105ee) #x0000000000000002))
(constraint (= (f #x06aa018dae2ca760) #x0000000000000002))
(constraint (= (f #xc921e7e27b72c091) #xfffffffffffffffd))
(constraint (= (f #x6abc5111322ec662) #x0000000000000002))
(constraint (= (f #x7822ee7a6ad49e4c) #x0000000000000002))
(constraint (= (f #xb9c3e9a3c2a04d8e) #x0000000000000002))
(constraint (= (f #x75937b1d0d90e516) #x0000000000000002))
(constraint (= (f #x4122e516d9e7ee67) #xfffffffffffffffd))
(constraint (= (f #x747031e111c61965) #xfffffffffffffffd))
(constraint (= (f #xeb7beb3916e2e23a) #x0000000000000002))
(constraint (= (f #x734d4244e41b8ac0) #x0000000000000002))
(constraint (= (f #xd9d7108d61151475) #xfffffffffffffffd))
(constraint (= (f #xaa71e756290879dc) #x0000000000000002))
(constraint (= (f #xee61ade6b450d70c) #x0000000000000002))
(constraint (= (f #xa38d806d21bb21be) #x0000000000000002))
(constraint (= (f #x72b179bc38176146) #x0000000000000002))
(constraint (= (f #xe35a5502cb1c3519) #xfffffffffffffffd))
(constraint (= (f #x66c291c13767ac56) #x0000000000000002))
(constraint (= (f #x4951483460ee5001) #xfffffffffffffffd))
(constraint (= (f #x33debe2aa78e8ddb) #xfffffffffffffffd))
(constraint (= (f #x44cd9400c0ae5a9e) #x0000000000000002))
(constraint (= (f #x8ce972eee830ae8c) #x0000000000000002))
(constraint (= (f #xe32834aa73120ab4) #x0000000000000002))
(constraint (= (f #xb2ae150e9aaa8ced) #xfffffffffffffffd))
(constraint (= (f #x26c2a87265035891) #xfffffffffffffffd))
(constraint (= (f #xd4819a868bb88107) #xfffffffffffffffd))
(constraint (= (f #x965ab1817d88662c) #x0000000000000002))
(constraint (= (f #xedb6d67e02e2905d) #xfffffffffffffffd))
(constraint (= (f #x14245626a7ed5e3a) #x0000000000000002))
(constraint (= (f #x0e2b0e8c8a88a36a) #x0000000000000002))
(constraint (= (f #x052959698e391195) #xfffffffffffffffd))
(constraint (= (f #xc86de8e07ee0b763) #xfffffffffffffffd))
(constraint (= (f #xd46a5d26300eea74) #x0000000000000002))
(constraint (= (f #x092735188b947c32) #x0000000000000002))
(constraint (= (f #xe34de78602c7b66e) #x0000000000000002))
(constraint (= (f #x12380e4740908a30) #x0000000000000002))
(constraint (= (f #xa35c31c11b8e44e3) #xfffffffffffffffd))
(constraint (= (f #x837e6669051a85e7) #xfffffffffffffffd))
(constraint (= (f #xe4e36c2aa4d6b885) #xfffffffffffffffd))
(constraint (= (f #x0ec785972ec0a216) #x0000000000000002))
(constraint (= (f #x67ed026058adeeca) #x0000000000000002))
(constraint (= (f #x895235418b634678) #x0000000000000002))
(constraint (= (f #xc52a560dd9e27834) #x0000000000000002))
(constraint (= (f #x8bbe45a3c10cac07) #xfffffffffffffffd))
(constraint (= (f #x208073a83ea19069) #xfffffffffffffffd))
(constraint (= (f #x730e2d98c5e8b1a9) #xfffffffffffffffd))
(constraint (= (f #xc0d2e980274c2ee6) #x0000000000000002))
(constraint (= (f #xe269882ce53e7e8e) #x0000000000000002))
(constraint (= (f #xa1a96217a7674d89) #xfffffffffffffffd))
(constraint (= (f #x7673bc3bd7c61b8d) #xfffffffffffffffd))
(constraint (= (f #xde93d553272a888c) #x0000000000000002))
(constraint (= (f #x90e97c983c611923) #xfffffffffffffffd))
(constraint (= (f #xe92556bbede9578d) #xfffffffffffffffd))
(constraint (= (f #xade0157ae3868883) #xfffffffffffffffd))
(constraint (= (f #x4e684d7bea5ba0a3) #xfffffffffffffffd))
(constraint (= (f #xc9012291b492c416) #x0000000000000002))
(constraint (= (f #x1393587992d61d23) #xfffffffffffffffd))
(constraint (= (f #xed728917ed62e4c7) #xfffffffffffffffd))
(constraint (= (f #x6e798a6a955565c0) #x0000000000000002))
(constraint (= (f #x885be593e999ca07) #xfffffffffffffffd))
(constraint (= (f #x3b394d2e344c3baa) #x0000000000000002))
(constraint (= (f #x017a5ee6e8d6be53) #xfffffffffffffffd))
(constraint (= (f #x161bee39292ea683) #xfffffffffffffffd))
(constraint (= (f #xe4e121220be5599a) #x0000000000000002))
(constraint (= (f #x3a4a3d3b8ea27a31) #xfffffffffffffffd))
(constraint (= (f #xdaec57a36224382c) #x0000000000000002))
(constraint (= (f #x879ebdaeb4e19d99) #xfffffffffffffffd))
(constraint (= (f #xac459b1105978740) #x0000000000000002))
(constraint (= (f #xea88e96e09e45e18) #x0000000000000002))
(constraint (= (f #x4e757ecc8b665e27) #xfffffffffffffffd))
(constraint (= (f #x4763c61b0b42e249) #xfffffffffffffffd))
(constraint (= (f #x535de86e6d4c4d06) #x0000000000000002))
(constraint (= (f #xe51c50d071e320d4) #x0000000000000002))
(constraint (= (f #x22889061453d83d8) #x0000000000000002))
(constraint (= (f #x1e580499e2aa78e8) #x0000000000000002))
(constraint (= (f #x4c50ac8d57ce8b4a) #x0000000000000002))
(constraint (= (f #xc9860ceed9e1615d) #xfffffffffffffffd))
(constraint (= (f #x6eee5588a2a56b77) #xfffffffffffffffd))
(constraint (= (f #xae16e8e615a18b4e) #x0000000000000002))
(constraint (= (f #xedd00381c398c05d) #xfffffffffffffffd))
(constraint (= (f #x585debc46b34de3a) #x0000000000000002))
(constraint (= (f #xe0deb58eba775600) #x0000000000000002))
(constraint (= (f #x10221b5059616b68) #x0000000000000002))
(constraint (= (f #x066e5bea13c060b3) #xfffffffffffffffd))
(constraint (= (f #xb72bc4e3802e7b9e) #x0000000000000002))
(constraint (= (f #xd9cd2e78d7d1bea4) #x0000000000000002))
(constraint (= (f #x95993c4b318e8121) #xfffffffffffffffd))
(constraint (= (f #x2a53c4e2e20cc418) #x0000000000000002))
(check-synth)
(define-fun f_1 ((x (BitVec 64))) (BitVec 64) (ite (= (bvor #x0000000000000001 x) x) (bvnot #x0000000000000002) #x0000000000000002))
